/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package chameleon.model.game.transition;

import chameleon.model.formula.Formula;
import chameleon.model.formula.parser.LtlParser;
import chameleon.model.game.Tag;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.FileWriter;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.util.logging.Level;
import java.util.logging.Logger;

/**
 * This class represents a transition relation described by an LTL formula.
 *
 *
 * @author simon
 */
public class Ltl extends TransitionRelationDescription {

    public Ltl(File ltlGame, int player){
        super(Tag.LTL);
        representation_ = ltlGame;
        player_ = player;
    }

    /**
     *  This method convert an LTL formula to a Nondeterministic Büchi Word (NBW)
     * vio Goal command.
     */

    @Override
    public void convert2NBW() {
        FileWriter fw = null;
        try {
            //First step, create a string that represents the formula
            String formula = convert2String(representation_);
            LtlParser parser = new LtlParser(formula);
            Formula inputFormula = parser.createFormula();
            formula = inputFormula.toString();
            //Second step: convert this string into a NBW
            File script = new File("script/convert2NBW");
            fw = new FileWriter(script);
            fw.write("#!/bin/bash\n");
            fw.write("GOAL-20110214/goal translate -m ltl2ba -t nbw -o ../GoalFile/ngbw.gff \"" + formula + "\"\n");
            fw.close();
            //CALL GOAL
            Runtime runtime = Runtime.getRuntime();
            runtime.exec("chmod u+x script/convert2NBW");
            Process p = runtime.exec(new String[]{"script/convert2NBW"});
            try {
                p.waitFor();
            } catch (InterruptedException ex) {
                Logger.getLogger(Ltl.class.getName()).log(Level.SEVERE, null, ex);
            }
            script.delete();
            representation_ =  new File("GoalFile/nbw"+player_+".gff");
        } catch (IOException ex) {
            Logger.getLogger(Ltl.class.getName()).log(Level.SEVERE, null, ex);
        } finally {
            try {
                fw.close();
            } catch (IOException ex) {
                Logger.getLogger(Ltl.class.getName()).log(Level.SEVERE, null, ex);
            }
        }
        File ngbw = new File ("GoalFile/ngbw.gff");
        ngbw.delete();
        isNBW_=true;
    }

    private String convert2String(File file) throws FileNotFoundException, IOException {
        InputStream ips = new FileInputStream(file);
        InputStreamReader ipsr = new InputStreamReader(ips);
        BufferedReader br = new BufferedReader(ipsr);

        String line,formula="";
        while((line = br.readLine())!=null){
            formula+=line;
        }

        return formula;

    }

    
}
